(* Copyright Per Lindgren 2015, see the file "LICENSE" *)
(* for the full license governing this code.           *)

(* FUN-4SURE/AST *)

open Common

type id   = int
type vid  = int
type eid  = int
type sid  = int
type aid  = int
type lval = int

type time = int

let st_of_id_env id = "{" ^ String.concat ", " (List.map Id.get_s id) ^ "}"
  
type bexpr =
  | OpAnd | OpOr  | OpExor 
  | OpMul | OpMod | OpDiv | OpAdd | OpSub 
  | OpEq  | OpNeq | OpLt | OpLEq | OpGt | OpGEq

type unop =
  | UNot 
  | UMinus
  
type expr =
  | OpExp     of bexpr * expr * expr
  | IdExp     of sid 
  | IntExp    of int
  | CharExp   of char
  | BoolExp   of bool 
  | UnOpExp   of unop * expr

type pType =
  | Int
  | Char
  | Bool
  | Byte
  
type ec_guard = 
  | EcGuard of time option * eid option * expr (* after? event? expr *)
  
let eo_of_gu    = function EcGuard (_, e, _) -> e
let time_of_gu  = function EcGuard (t, _, _) -> t 
let exp_of_gu   = function EcGuard (_, _, x) -> x   

type ec_trans =
  | EcTrans of sid * sid * ec_guard
  
let gu_of_tr    = function EcTrans (_, _, g) -> g 
let sd_of_tr    = function EcTrans (s, d, _) -> (s, d) 
let eid_of_tr   = function EcTrans (_, _, EcGuard (_, ido, _)) -> ido
                                                       
type ec_action =
  | EcAction of aid option * eid list 
   
let eid_of_act  = function EcAction (_, eidl) -> eidl 
let aid_of_act  = function EcAction (aidl,_)  -> aidl

        
type ec_state =
  | EcState of sid * ec_action list
       
let sid_of_st   = function EcState (sid ,_)  -> sid
let act_of_st   = function EcState (_, actl) -> actl
      
type contract =
  | Requires of expr
  | Ensures  of expr
  | ReqRaw   of string
  | EnsRaw   of string
    
type fb_ecc = 
  | FbEcc   of  ec_state list * contract list * ec_trans list 

let co_of_ecc   = function FbEcc (co, _, _) -> co
let sl_of_ecc   = function FbEcc (_, sl, _) -> sl
let tr_of_ecc   = function FbEcc (_, _, tr) -> tr

type var =
  | Var of vid * pType

let id_of_va    = function Var (id, _) -> id 
let t_of_va     = function Var (_, t)  -> t
let v_of_va     = function Var (id, v) -> (id, v) 
  
type st_stmt =
  | StmtAssign of lval * expr
  | StmtAssert of expr
  
type fb_alg =
  | FbAlg of aid * contract list * var list * st_stmt list 

let id_of_alg   = function FbAlg (id,_ , _, _) -> id

type event =
  | Event of eid * eid option * (eid list) option 
  
let id_of_e     = function Event (id, _, _)       -> id   
(* let et_of_e     = function Event (_, Some et, _)  -> et   *)
let wio_of_e    = function Event (_, et, wi) -> wi   

(* input events, output events, input vars, ouptut vars *)
type fb_if = 
  | FbIf of event list * event list * var list * var list   

let eil_of_if   = function FbIf (el, _, _, _) -> el 
let eol_of_if   = function FbIf (_ ,el, _, _) -> el
let vil_of_if   = function FbIf (_ ,_ ,vl, _) -> vl
let vol_of_if   = function FbIf (_ ,_ , _,vl) -> vl

(* internal variables *)
type fb_var =
  | FbVar of var list   

let vl_of_v     = function FbVar (vl) -> vl
let v_of_fb_v   = function FbVar (v)  -> v

type top =
  | FB       of int * fb_if * fb_var * fb_ecc option * fb_alg list                                         

